/**
 * Software Analysis and Verification 
 * @project: Verify Pattern Matching with Guards in Scala
 * @authors: Mirco Dotta and Philippe Suter
 */

package ch.epfl.lara.patterns.analyze;

import ch.epfl.lara.patterns.ast._

import ch.epfl.lara.patterns.utils.FreshNameCreator._

import scala.collection.immutable.{Map,HashMap}

import ch.epfl.lara.patterns.decider.FormulaDecider

import ch.epfl.lara.patterns.utils.FormulaSimplifier

object Verifier extends FormulaWrapper with Constants {
  
  type Env = HierarchyHolder
  type TypedVar = (String,String)
  
  private var formDecider: FormulaDecider = null

  def setFormulaDecider(fd: FormulaDecider): Unit = {
	formDecider = fd
	if(!formDecider.init) {
		Console.err.println("Could not initialize the formula decider.")
	}
  }

  /**
   * <p>
   *        Build the formula that correspond to the analyzed pattern.
   * </p>
   * @param env     : Environment contains the whole hierarchy tree of the pattern expression.
   * @param selector: The selector of the matched block (e.g. 'selector' match { case _ => ... }).
   * @param pattern : Pattern is the one matched class or object.
   * @return        : The derived formula that correspond to the pattern gave in argument.
   */
  private def buildFormula(env: Env, selector: Element, pattern: Pattern, join: (Formula, Formula) => Formula): Formula = {
    def build(klass: KlassPattern) = 
      join(buildBindingsFormula(env,selector,klass), buildPatternFormula(env,selector,pattern,join))
    
    pattern match {
      case GuardedKlass(klass, guard) => 
        build(klass)
      case klass @ Klass(_,_) => 
        build(klass)
        
      case SimpleArgument(name, typez) => 
             And(Equal(selector,Var(name)),In(Var(name),VarSet(typez)))
             
      case Objekt(_) | Wildcard => buildPatternFormula(env,selector,pattern,join)
    }
  }
  
  private def buildPatternFormula (env: Env, selector: Element, pattern: Pattern, join: (Formula, Formula) => Formula) : Formula = pattern match {
     case GuardedKlass(klass, guard) => And(buildFormula(env, selector, klass, join), guard.getFormula)
     
     case Klass(name, args) => 
       val argsAndFields = args.zip(env.lookupKlass(name).fields)
       val argsFormula: List[Formula] = for( val (arg,FieldDef(fname,ftype)) <- argsAndFields) yield {
         val accessor = name + FUNC_NAME_SEP + fname
         val functcall = FunctionCall(Var(accessor), selector)
         arg match {
           case SimpleArgument(sident,stype) =>  
             In(Var(sident),VarSet(stype))
           
           case klassArg @ _ if(klassArg.isInstanceOf[KlassPattern]) =>  // this couldn't be a guarded pattern !
             buildFormula(env,functcall,klassArg.asInstanceOf[KlassPattern],join)
         }
         
       }
       And(In(selector,VarSet(name)),CNF(argsFormula))
     
     case Objekt(name) => 
       In(selector,VarSet(name))
     
     case Wildcard => True
  }
   
   private def buildBindingsFormula(env: Env, selector: Element, pattern: KlassPattern) : Formula = pattern match { 
     case Klass(name, args) => 
       val argsAndFields = args.zip(env.lookupKlass(name).fields)
       val argsFormula: List[Formula] = for( val (arg,FieldDef(fname,ftype)) <- argsAndFields) yield {
         val accessor = name + FUNC_NAME_SEP + fname
         val functcall = FunctionCall(Var(accessor), selector)
         arg match {
           case SimpleArgument(sident,stype) =>  
             Equal(Var(sident),functcall) 
         
           case klassArg @ _ if(klassArg.isInstanceOf[KlassPattern]) =>  // this couldn't be a guarded pattern !
             buildBindingsFormula(env,functcall,klassArg.asInstanceOf[KlassPattern])
         }
       }
       CNF(argsFormula)
       
     case Objekt(_) | Wildcard => True
     
     case SimpleArgument(name, typez) => 
     	And(Equal(selector,Var(name)),In(Var(name),VarSet(typez)))
   }
  
  
  /**
   * 
   *
   */ 
  //XXX: Remember to call Renamer object on Match before executing this method!
  def buildCompletenessFormula (env: Env, matsch: Match) : Formula = (matsch: @unchecked) match {
    case Match(selector @ (sname,stype),patterns) => 
      FormulaSimplifier(Imply( generateAxioms(env, selector), DNF(patterns.map(kase => buildFormula(env,Var(sname),kase, {(f1:Formula,f2:Formula) => Imply(f1, f2)} ))))) 
    
  }
  
  //XXX: TO be implemented
  def buildDisjointnessFormula (env: Env, matsch: Match) : Formula = (matsch: @unchecked) match {
    case Match(selector @ (sname, stype), patterns) =>
       val patternFormulas = patterns.map(kase => buildFormula(env,Var(sname),kase, {(f1:Formula,f2:Formula) => And(f1, f2)}))
      
      val disjointnessForm = CNF(             
           for(val c <- List.range(0, patternFormulas.length - 1); val k2 <- patternFormulas.drop(c + 1)) yield Not(And(patternFormulas(c), k2))
      )

/*
	A potential simplification, untested at this point
	  def buildForm(p: Pattern): Formula =
	  	buildFormula(env, Var(sname), p, (f1:Formula,f2:Formula) => And(f1, f2))
      
	  def rootClass(p: Pattern): String = p match {
		case GuardedKlass(k, g) => rootClass(k)
		case Klass(n, _) => n
		case Objekt(n) => n
		case SimpleArgument(_, t) => t
		case _ => "unknown"
	  }
	  
	  val disjointnessForm = CNF(
		for(val i <- List.range(0, patterns.length - 1); val p2 <- patterns.drop(i + 1)) yield {
			val p1 = patterns(i)
			val r1 = rootClass(p1)
			val r2 = rootClass(p2)

			if(p1.equals("unknown") || p2.equals("unknown") || p1.equals(p2)) {
				Not(And(buildForm(p1), buildForm(p2)))
			} else {
				True
			}
		}	
	  )
	  */
	  
      FormulaSimplifier(Imply(generateAxioms(env, selector), disjointnessForm))
  }
  
   
  //TO Implement
  def isFormulaCorrect (formula: Formula) : Boolean = 
    /* 
      2. Give formula to formDecider to verify correctness of generated formula
      3. Output result of isabelle (either correct formula or incorrect/undecidable)
    */
	if(formDecider != null) {
		formDecider.decide(formula.toString)
	} else {
		Console.err.println("The formula decider was never set or initialized.")
		false
	}
    
  //TO Implement ...
  def isComplete(env: Env, m: Match) : Boolean  = 
      isFormulaCorrect(buildCompletenessFormula(env, m))
      
  // TO Implement ...
  def isDisjoint(env: Env, m: Match) : Boolean  =
      isFormulaCorrect(buildDisjointnessFormula(env, m))
      
  def isPartitioned (env: Env, m: Match) : Boolean  = isComplete(env, m) && isDisjoint(env, m)
    
    
  /**
   * <p> 
   *         Create a formula that represents all possible types that a variable can have.
   *    In order to make valuable formulas, the class constructor and arguments type 
   *    of the constructor must be taken in consideration.
   * </p>
   * @param Env: Represents all posible types that the variable can have
   * @param variable: The variable that we are interested in.
   * @return: A formula that represents all possible (so complete) types the 
   *              variable could have.
   */
  def generateAxioms(env: Env, selector: (String,String)) : Formula = 
    CNF(generatePrimitiveAxioms ::
        generateObjectAxioms(env) ::
        generateTypeAxioms(env)  ::
        generateFieldsAxioms(env) ::
        generateSelectorAxioms(env, selector) ::
        Nil)
   
   /** Generates trivial equalities for case objects, such as Leaf = { Leaf0 } */
   def generateObjectAxioms(env: Env) : Formula = {
     val objects = env.getHierarchy.values.toList.filter(o => o.isObject).map(o => o.name)
     
     CNF(objects.map(o => Equal(VarSet(o), Singleton(Var(shortFresh(o))))))
   }
    
   def generateTypeAxioms(env: Env) : Formula = {
     def generateRootAxiom(klass: HierarchyKlass, children: List[HierarchyKlass]) : Formula = {
       val varr = Var(shortFresh(klass.name))
       
       // retrieves the list of non-abstract subclasses...
       val subs = env.getKlassDescendants(klass.name).remove(k => k.isAbstract)
       
       val completenessCond = DNF(subs.map(s => In(varr, VarSet(s.name))))
       
       val disjointnessCond = CNF(             
           for(val c <- List.range(0, children.length - 1); val k2 <- children.drop(c + 1)) yield Not(And(In(varr, VarSet(children(c).name)), In(varr, VarSet(k2.name))))
       )
       
       Forall(varr, Imply(In(varr, VarSet(klass.name)), And(completenessCond, disjointnessCond)))
     }
     
     def acc(klasses: List[HierarchyKlass]): List[Formula] = klasses match {
       case Nil => Nil
       case x :: xs => {
         val children = env.getKlassChildren(x.name)
         if (children.isEmpty)
           acc(xs)
         else
           generateRootAxiom(x, children) :: acc(xs)
       }
     }

     // we generate formulas for dependencies for all classes which are not case classes..
     CNF(acc(env.getHierarchy.values.toList))
   }
   
   def generateSelectorAxioms(env: Env, selector: (String,String)) : Formula = {
     val (sName, sKlass) = selector
    
     //XXX:
     In(Var(sName), VarSet(sKlass))
   }
   
   def generateFieldsAxioms(env: Env): Formula = {
     def generateCaseKlassAxioms(klass: HierarchyKlass): Formula = {
       val varr = shortFresh(klass.name)
       
       val insideCond : List[Formula] = for(val f <- klass.fields) yield {
         val functionName = klass.name + FUNC_NAME_SEP + f.name
         In(FunctionCall(Var(functionName), Var(varr)), VarSet(f.typez))
       }
       
       Forall(Var(varr), Imply(In(Var(varr), VarSet(klass.name)), CNF(insideCond)))
     }
     
     /* we're looking at the only classes with fields in which we are intestered, namely the case classes */
     val caseKlasses = env.getHierarchy.values.toList.filter(k => k.isCase && !k.isObject)
     
     CNF(caseKlasses.map(generateCaseKlassAxioms))
   }
   
   
   def generatePrimitiveAxioms : Formula = {
     val varr = "v"
     Forall(Var(varr), Imply(In(Var(varr),VarSet("PrimitiveInt")), Or(LessEq(TypedVar(varr,"int"), IntValue(0)), Less(IntValue(0),TypedVar(varr,"int")))))
   }
 
}
